T:(IdType), tab:secret-table(T).
atoms-distinct(tab)
 (x:Atom1, n:{0..||tab|| }.
 (n  ptr(tab))
  (st-atom(tab;n) = x)
  ((isl(st-lookup(tab;x)))
  c (outl(st-lookup(tab;x)) = <key(tab;n), data(tab;n)>  (:( + Atom1)  data(T))))) 

latex

Definitions	A c B, Type, t  T, Id, x:AB(x), x:A. B(x), secret-table(T), atoms-distinct(tab), Atom$n, , {x:A| B(x)} , ||tab|| , #$n, {i..j}, ptr(tab), A  B, st-atom(tab;n), s = t, , P  Q, x:A  B(x), P & Q, x:A. B(x), a < b, Void, False, A, i  j < k, , P  Q, P  Q, <a, b>, {T}, SQType(T), s ~ t, data(tab;n), key(tab;n), left + right, data(T), Unit, st-lookup(tab;x), outl(x)
Lemmas	st-lookup-outl, st-lookup-property, st-atom wf, le wf, st-ptr wf, int seg wf, st-length wf, nat wf, st-atoms-distinct wf, secret-table wf, Id wf